Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    minus(X,0)  → X
2:    minus(s(X),s(Y))  → p(minus(X,Y))
3:    p(s(X))  → X
4:    div(0,s(Y))  → 0
5:    div(s(X),s(Y))  → s(div(minus(X,Y),s(Y)))
There are 4 dependency pairs:
6:    MINUS(s(X),s(Y))  → P(minus(X,Y))
7:    MINUS(s(X),s(Y))  → MINUS(X,Y)
8:    DIV(s(X),s(Y))  → DIV(minus(X,Y),s(Y))
9:    DIV(s(X),s(Y))  → MINUS(X,Y)
The approximated dependency graph contains 2 SCCs: {7} and {8}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006